A:Type, eq:EqDecider(A), P:(ATypeProp), f, g:x:A fp Type.
ydom(f). w=f(y)   P(y,w)
 ydom(g). w=g(y)   P(y,w)
 ydom(f  g). w=f  g(y)   P(y,w) 

latex

Definitions	False, x,y. t(x;y), EqDecider(T), f  g, a:A fp B(a), x. t(x), Top, Unit, P  Q, P & Q, x  dom(f), , Prop, b, A, x(s1,s2), xdom(f). v=f(x)   P(x;v), P  Q, t  T, P  Q, x:A. B(x), b
Lemmas	assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-ap-sq, fpf-join-dom2, fpf-trivial-subtype-top, top wf, fpf-join wf, deq wf, fpf wf, fpf-all wf